\begin{tabbing}
$\forall$${\it es}$:ES.
\\[0ex]es{-}Send(${\it es}$)
\\[0ex]$\in$ \=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.es{-}V(${\it es}$)($i$,$a$); $l$,$t$.es{-}M(${\it es}$)($l$,$t$) )$\rightarrow$state@$i$$\rightarrow$\+
\\[0ex](Msg(es{-}M(${\it es}$)) List)
\-
\end{tabbing}